Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(g(X),Y)  → f(X,n__f(n__g(X),activate(Y)))
2:    f(X1,X2)  → n__f(X1,X2)
3:    g(X)  → n__g(X)
4:    activate(n__f(X1,X2))  → f(activate(X1),X2)
5:    activate(n__g(X))  → g(activate(X))
6:    activate(X)  → X
There are 6 dependency pairs:
7:    F(g(X),Y)  → F(X,n__f(n__g(X),activate(Y)))
8:    F(g(X),Y)  → ACTIVATE(Y)
9:    ACTIVATE(n__f(X1,X2))  → F(activate(X1),X2)
10:    ACTIVATE(n__f(X1,X2))  → ACTIVATE(X1)
11:    ACTIVATE(n__g(X))  → G(activate(X))
12:    ACTIVATE(n__g(X))  → ACTIVATE(X)
The approximated dependency graph contains one SCC: {7-10,12}.
Tyrolean Termination Tool  (0.10 seconds)   ---  May 3, 2006